(VERS1 0 (NIL ((LINENAME SORTINFO (LN& #& . 0) (LN& #& . 22) (LN& #& . 35) (LN& #& . 36) (LN& #& . 40) (LN& #& . 41) (LN& #& . 42) (LN& #& . 46)) (LINENAME SIMPINFO (LN& #& . 22) (LN& #& . 50) (LN& #& . 58) (LN& #& . 59) (LN& #& . 60) (LN& #& . 66) (LN& #& . 67) (LN& #& . 68) (LN& #& . 69) (LN& #& . 70) (LN& #& . 71) (LN& #& . 72) (LN& #& . 73)) (LINENAME CONSFACTS (LN& #& . 58) (LN& #& . 59) (LN& #& . 67) (LN& #& . 68)) (LINENAME LISTINDUCTION (LN& #& . 74)) (LINENAME SEXPINDUCTION (LN& #& . 77)) (LINENAME LISTAPPEND (LN& #& . 42)) (LINENAME DEFINFO (LN& #& . 78) (LN& #& . 79) (LN& #& . 89) (LN& #& . 92) (LN& #& . 93) (LN& #& . 96)) (LINENAME APPENDFACTS (LN& #& . 72) (LN& #& . 73)) (LINENAME REVERSEAPPEND (LN& #& . 99))) (REVERS (#& . 98) (#& . 96) (#& . 100) (#& . 101) (#& . 102) (#& . 103) (#& . 104) (#& . 105) (#& . 106) (#& . 107)) (LISPAX (#& . 2) (#& . 30) (#& . 108) (#& . 76) (#& . 52) (#& . 112) (#& . 27) (#& . 62) (#& . 54) (#& . 24) (#& . 20) (#& . 0) (#& . 114) (#& . 22) (#& . 115) (#& . 116) (#& . 50) (#& . 117) (#& . 35) (#& . 118) (#& . 58) (#& . 119) (#& . 59) (#& . 120) (#& . 60) (#& . 121) (#& . 66) (#& . 122) (#& . 67) (#& . 123) (#& . 68) (#& . 124) (#& . 74) (#& . 125) (#& . 77) (#& . 126) (#& . 38) (#& . 36) (#& . 127) (#& . 69) (#& . 128) (#& . 40) (#& . 129) (#& . 70) (#& . 130) (#& . 41) (#& . 131) (#& . 71) (#& . 132) (#& . 44) (#& . 42) (#& . 133) (#& . 78) (#& . 134) (#& . 72) (#& . 135) (#& . 73) (#& . 136) (#& . 81) (#& . 88) (#& . 79) (#& . 137) (#& . 91) (#& . 89) (#& . 138) (#& . 48) (#& . 46) (#& . 139) (#& . 92) (#& . 140) (#& . 99) (#& . 141) (#& . 142) (#& . 95) (#& . 93) (#& . 143))) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 76 .) ((((∀ U)) (= (REVERSE (REVERSE U)) U)) . (AXIOM (TM& ((∀ U)) (= (REVERSE (REVERSE U)) U))) . NIL . ((REVERSE #& . 47) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 73 .) (NIL . (COMMENTL LNAME REVERSEAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 72 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 70 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 68 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 65 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 62 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 58 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 56 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 54 .) (NIL . (COMMENTL LNAME SORTINFO LISTAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 52 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 49 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 47 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 45 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 43 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 41 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 39 .) (NIL . (COMMENTL LNAME SEXPINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 36 .) (NIL . (COMMENTL LNAME LISTINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 34 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 32 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 30 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 28 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 26 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 24 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 22 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 20 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 18 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U #& . 1) (NNIL #& . 51) (NULL #& . 53)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 16 .) (NIL . (COMMENTL LNAME SORTINFO SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 15 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 13 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 112) . CONS .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS #& . 113)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 6 .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 108) . B .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 108) . A .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 108) . C .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((C #& . 109) (A #& . 110) (B #& . 111)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 3 .) ((((∀ U V)) (= (REV1 U V) (* (REVERSE U) V))) . (RW (LN& #& . 101) (MODE& * ($ LR& (#& . 106)) (STANDARD))) . NIL . ((U #& . 1) (V #& . 14) (REVERSE #& . 47) (REV1 #& . 97)) . ((* #& . 43)) . NIL . ((#& . 74) (#& . 50) (#& . 58) (#& . 59) (#& . 60) (#& . 66) (#& . 67) (#& . 68) (#& . 69) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96) (#& . 46) (#& . 42) (#& . 41) (#& . 40) (#& . 36) (#& . 35) (#& . 22) (#& . 0)) . NIL . REVERS . NIL . NIL . 10 .) ((((∀ X U)) (⊃ (((∀ V)) (= (REV1 U V) (* (REVERSE U) V))) (((∀ V)) (= (REV1 U (~ X V)) (* (REVERSE U) (~ X V)))))) . (∀I (X U) (LN& #& . 105)) . NIL . ((U #& . 1) (~ #& . 26) (X #& . 29) (V #& . 14) (REVERSE #& . 47) (REV1 #& . 97)) . ((* #& . 43)) . NIL . ((#& . 46) (#& . 42) (#& . 41) (#& . 40) (#& . 36) (#& . 35) (#& . 22) (#& . 0)) . NIL . REVERS . NIL . NIL . 9 .) ((⊃ (((∀ V)) (= (REV1 U V) (* (REVERSE U) V))) (((∀ V)) (= (REV1 U (~ X V)) (* (REVERSE U) (~ X V))))) . (CI ((LR& (#& . 102))) (LN& #& . 104) (MODE& STANDARD)) . NIL . ((U #& . 1) (~ #& . 26) (X #& . 29) (V #& . 14) (REVERSE #& . 47) (REV1 #& . 97)) . ((* #& . 43)) . NIL . ((#& . 46) (#& . 42) (#& . 41) (#& . 40) (#& . 36) (#& . 35) (#& . 22) (#& . 0)) . NIL . REVERS . NIL . NIL . 8 .) ((((∀ V)) (= (REV1 U (~ X V)) (* (REVERSE U) (~ X V)))) . (∀I (V) (LN& #& . 103)) . NIL . ((U #& . 1) (~ #& . 26) (X #& . 29) (V #& . 14) (REVERSE #& . 47) (REV1 #& . 97)) . ((* #& . 43)) . NIL . ((#& . 0) (#& . 22) (#& . 35) (#& . 36) (#& . 40) (#& . 41) (#& . 42) (#& . 46) (#& . 102)) . NIL . REVERS . NIL . NIL . 7 .) ((= (REV1 U (~ X V)) (* (REVERSE U) (~ X V))) . (TRW (TM& REV1 U (~ X V)) (MODE& LR& (#& . 102)) (LR& (#& . 0) (#& . 22) (#& . 35) (#& . 36) (#& . 40) (#& . 41) (#& . 42) (#& . 46))) . NIL . ((U #& . 1) (~ #& . 26) (X #& . 29) (V #& . 14) (REVERSE #& . 47) (REV1 #& . 97)) . ((* #& . 43)) . NIL . ((#& . 0) (#& . 22) (#& . 35) (#& . 36) (#& . 40) (#& . 41) (#& . 42) (#& . 46) (#& . 102)) . NIL . REVERS . NIL . NIL . 6 .) ((((∀ V)) (= (REV1 U V) (* (REVERSE U) V))) . (ASSUME (TM& ((∀ V)) (= (REV1 U V) (* (REVERSE U) V)))) . NIL . ((U #& . 1) (V #& . 14) (REVERSE #& . 47) (REV1 #& . 97)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . REVERS . NIL . NIL . 5 .) ((⊃ (((∀ X U)) (⊃ (((∀ V)) (= (REV1 U V) (* (REVERSE U) V))) (((∀ V)) (= (REV1 U (~ X V)) (* (REVERSE U) (~ X V)))))) (((∀ U V)) (= (REV1 U V) (* (REVERSE U) V)))) . (∀E PHI (TM& ((λ U)) (((∀ V)) (= (REV1 U V) (* (REVERSE U) V)))) (LN& #& . 74) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 22) (#& . 50) (#& . 58) (#& . 59) (#& . 60) (#& . 66) (#& . 67) (#& . 68) (#& . 69) (#& . 70) (#& . 71) (#& . 72) (#& . 73)) (STANDARD)) (STANDARD) ((PART ((1 1 2))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 22) (#& . 50) (#& . 58) (#& . 59) (#& . 60) (#& . 66) (#& . 67) (#& . 68) (#& . 69) (#& . 70) (#& . 71) (#& . 72) (#& . 73)) (STANDARD)) (STANDARD)) (LR& (#& . 0) (#& . 22) (#& . 35) (#& . 36) (#& . 40) (#& . 41) (#& . 42) (#& . 46))) . NIL . ((U #& . 1) (X #& . 29) (~ #& . 26) (V #& . 14) (REVERSE #& . 47) (REV1 #& . 97)) . ((* #& . 43)) . NIL . ((#& . 74) (#& . 0) (#& . 35) (#& . 36) (#& . 40) (#& . 41) (#& . 42) (#& . 46) (#& . 22) (#& . 50) (#& . 58) (#& . 59) (#& . 60) (#& . 66) (#& . 67) (#& . 68) (#& . 69) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . REVERS . NIL . NIL . 4 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . REVERS . NIL . NIL . 3 .) ((((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U)))) . (AXIOM (TM& ((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U))))) . NIL . ((V #& . 14) (U #& . 1) (REVERSE #& . 47)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 71 .) (NIL . (DECL (REV1) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((REV1 #& . 97)) . NIL . NIL . NIL . NIL . REVERS . NIL . NIL . 1 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 98) . REV1 .) ((((∀ U V)) (= (REV1 U V) (CONDI (NULL U) V (REV1 (CDR U) (~ (CAR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (REV1 U V) (CONDI (NULL U) V (REV1 (CDR U) (~ (CAR U) V)))))) . NIL . ((~ #& . 26) (CAR #& . 61) (CDR #& . 63) (U #& . 1) (V #& . 14) (NULL #& . 53) (REV1 #& . 97)) . NIL . NIL . ((&& . 1)) . NIL . REVERS . NIL . NIL . 2 .) (NIL . (DECL (SUBST) (OT& (GROUND GROUND GROUND) . GROUND) CONSTANT) . NIL . ((SUBST #& . 94)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 74 .) (CONSTANT . ((GROUND GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 95) . SUBST .) ((((∀ X Y Z)) (= (SUBST X Y Z) (CONDI (ATOM Z) (CONDI (= Z Y) X Z) (~ (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z)))))) . (AXIOM (TM& ((∀ X Y Z)) (= (SUBST X Y Z) (CONDI (ATOM Z) (CONDI (= Z Y) X Z) (~ (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))) . NIL . ((ATOM #& . 55) (CDR #& . 63) (CAR #& . 61) (~ #& . 26) (Z #& . 31) (X #& . 29) (Y #& . 34) (SUBST #& . 94)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 75 .) ((((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U)))))) . (AXIOM (TM& ((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U))))))) . NIL . ((REVERSE #& . 47) (NULL #& . 53) (CDR #& . 63) (CAR #& . 61) (NNIL #& . 51) (U #& . 1)) . ((LIST #& . 37) (* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 69 .) (NIL . (DECL (MEMBER) (OT& (GROUND GROUND) . TRUTHVAL) CONSTANT) . NIL . ((MEMBER #& . 90)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 63 .) (CONSTANT . ((GROUND GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 91) . MEMBER .) ((((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U)))))) . (AXIOM (TM& ((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U))))))) . NIL . ((NULL #& . 53) (CDR #& . 63) (CAR #& . 61) (X #& . 29) (U #& . 1) (MEMBER #& . 90)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 64 .) (NIL . (DECL (ASSOC) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((ASSOC #& . 87)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 60 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 88) . ASSOC .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . A1 .) (6 . ALISTP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 85) . (#& . 81) . ALISTP .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . A0 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . A2 .) (NIL . (DECL (ALIST A0 A1 A2) (OT& . GROUND) VARIABLE ALISTP) . NIL . ((A2 #& . 82) (A0 #& . 83) (ALISTP #& . 84) (ALIST #& . 80) (A1 #& . 86)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 59 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . ALIST .) ((((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST)))))) . (AXIOM (TM& ((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST))))))) . NIL . ((X #& . 29) (NNIL #& . 51) (CAR #& . 61) (CDR #& . 63) (NULL #& . 53) (ALIST #& . 80) (ASSOC #& . 87)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 61 .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V)))))) . NIL . ((NULL #& . 53) (CDR #& . 63) (CAR #& . 61) (~ #& . 26) (U #& . 1) (V #& . 14)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 53 .) ((((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X))))) . NIL . ((ATOM #& . 55) (~ #& . 26) (PHI #& . 75) (X #& . 29) (Y #& . 34)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 35 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI #& . 75)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 4 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 76) . PHI .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U))))) . NIL . ((U #& . 1) (X #& . 29) (PHI #& . 75) (NNIL #& . 51) (~ #& . 26)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 33 .) ((((∀ X U V)) (= (* (~ X U) V) (~ X (* U V)))) . (AXIOM (TM& ((∀ X U V)) (= (* (~ X U) V) (~ X (* U V))))) . NIL . ((~ #& . 26) (X #& . 29) (U #& . 1) (V #& . 14)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 57 .) ((((∀ U)) (= (* NNIL U) U)) . (AXIOM (TM& ((∀ U)) (= (* NNIL U) U))) . NIL . ((U #& . 1) (NNIL #& . 51)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 55 .) ((((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z)))) . (AXIOM (TM& ((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z))))) . NIL . ((~ #& . 26) (Z #& . 31) (X #& . 29) (Y #& . 34)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 48 .) ((((∀ X Y)) (= (LIST X Y) (~ X (LIST Y)))) . (AXIOM (TM& ((∀ X Y)) (= (LIST X Y) (~ X (LIST Y))))) . NIL . ((~ #& . 26) (X #& . 29) (Y #& . 34)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 44 .) ((((∀ X)) (= (LIST X) (~ X NNIL))) . (AXIOM (TM& ((∀ X)) (= (LIST X) (~ X NNIL)))) . NIL . ((~ #& . 26) (NNIL #& . 51) (X #& . 29)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 40 .) ((((∀ X Y)) (= (CDR (~ X Y)) Y)) . (AXIOM (TM& ((∀ X Y)) (= (CDR (~ X Y)) Y))) . NIL . ((CDR #& . 63) (~ #& . 26) (X #& . 29) (Y #& . 34)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 31 .) ((((∀ X Y)) (= (CAR (~ X Y)) X)) . (AXIOM (TM& ((∀ X Y)) (= (CAR (~ X Y)) X))) . NIL . ((Y #& . 34) (X #& . 29) (~ #& . 26) (CAR #& . 61)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 29 .) ((((∀ X U)) (= (CDR (~ X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (~ X U)) U))) . NIL . ((CDR #& . 63) (~ #& . 26) (X #& . 29) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 27 .) (4 . |CAR | . UNARY . 950 .) (4 . |CDR | . UNARY . 950 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 64) . (#& . 62) . CDR .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((CDR #& . 63) (CAR #& . 61)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 8 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 65) . (#& . 62) . CAR .) ((((∀ X U)) (= (CAR (~ X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (~ X U)) X))) . NIL . ((U #& . 1) (X #& . 29) (~ #& . 26) (CAR #& . 61)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 25 .) ((((∀ X U)) (¬ (NULL (~ X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (~ X U))))) . NIL . ((NULL #& . 53) (~ #& . 26) (X #& . 29) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 23 .) ((((∀ X Y)) (¬ (ATOM (~ X Y)))) . (AXIOM (TM& ((∀ X Y)) (¬ (ATOM (~ X Y))))) . NIL . ((Y #& . 34) (X #& . 29) (~ #& . 26) (ATOM #& . 55)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 21 .) (5 . |NULL | . UNARY . 750 .) (5 . |ATOM | . UNARY . 750 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 56) . (#& . 54) . ATOM .) (NIL . (DECL (ATOM NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((NULL #& . 53) (ATOM #& . 55)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 9 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 57) . (#& . 54) . NULL .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LISTP) . NIL . ((NNIL #& . 51) (LISTP #& . 10)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 5 .) (CONSTANT . GROUND . LISTP . NIL . NIL . (#& . 52) . NNIL .) ((NULL NNIL) . (AXIOM (TM& NULL NNIL)) . NIL . ((NNIL #& . 51) (NULL #& . 53)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 17 .) (8 . |REVERSE | . UNARY . 950 .) (NIL . (DECL (REVERSE) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((REVERSE #& . 47)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 66 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 49) . (#& . 48) . REVERSE .) ((((∀ U)) (LISTP (REVERSE U))) . (AXIOM (TM& ((∀ U)) (LISTP (REVERSE U)))) . NIL . ((U #& . 1) (LISTP #& . 23) (REVERSE #& . 47)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 67 .) (1 . * . INFIX . 840 .) (NIL . (DECL (*) (FT& ((GROUND GROUND) GROUND NIL . GROUND)) FUNCTIONAL NIL INFIX 840 BOTH) . NIL . NIL . ((* #& . 43)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 50 .) (FUNCTIONAL . (((GROUND GROUND) GROUND NIL . GROUND)) . UNIVERSAL . BOTH . (#& . 45) . (#& . 44) . * .) ((((∀ U V)) (LISTP (* U V))) . (AXIOM (TM& ((∀ U V)) (LISTP (* U V)))) . NIL . ((V #& . 14) (U #& . 1) (LISTP #& . 23)) . ((* #& . 43)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 51 .) ((((∀ X Y Z)) (LISTP (LIST X Y Z))) . (AXIOM (TM& ((∀ X Y Z)) (LISTP (LIST X Y Z)))) . NIL . ((Y #& . 34) (X #& . 29) (Z #& . 31) (LISTP #& . 23)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 46 .) ((((∀ X Y)) (LISTP (LIST X Y))) . (AXIOM (TM& ((∀ X Y)) (LISTP (LIST X Y)))) . NIL . ((Y #& . 34) (X #& . 29) (LISTP #& . 23)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 42 .) (4 . LIST . PREFIX . 1000 .) (NIL . (DECL (LIST) (FT& ((GROUND) GROUND NIL . GROUND)) FUNCTIONAL) . NIL . NIL . ((LIST #& . 37)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 37 .) (FUNCTIONAL . (((GROUND) GROUND NIL . GROUND)) . UNIVERSAL . NIL . (#& . 39) . (#& . 38) . LIST .) ((((∀ X)) (LISTP (LIST X))) . (AXIOM (TM& ((∀ X)) (LISTP (LIST X)))) . NIL . ((X #& . 29) (LISTP #& . 23)) . ((LIST #& . 37)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 38 .) ((((∀ X Y)) (SEXP (~ X Y))) . (AXIOM (TM& ((∀ X Y)) (SEXP (~ X Y)))) . NIL . ((SEXP #& . 19) (~ #& . 26) (X #& . 29) (Y #& . 34)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 19 .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 30) . Y .) (4 . SEXP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 33) . (#& . 30) . SEXP .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 30) . Z .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z #& . 31) (X #& . 29) (SEXP #& . 32) (Y #& . 34)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 2 .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 30) . X .) (1 . ~ . INFIX . 850 .) (NIL . (DECL (~) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL INFIX 850) . NIL . ((~ #& . 26)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 7 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 28) . (#& . 27) . ~ .) (6 . |LISTP | . UNARY . 750 .) (NIL . (DECL (LISTP) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((LISTP #& . 23)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 10 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 25) . (#& . 24) . LISTP .) ((((∀ X U)) (LISTP (~ X U))) . (AXIOM (TM& ((∀ X U)) (LISTP (~ X U)))) . NIL . ((LISTP #& . 23) (~ #& . 26) (X #& . 29) (U #& . 1)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 14 .) (5 . |SEXP | . UNARY . 750 .) (NIL . (DECL (SEXP) (OT& (CROUND) . TRUTHVAL) CONSTANT NIL UNARY 710) . NIL . ((SEXP #& . 19)) . NIL . NIL . NIL . LIL . LISPAX . LIL . NIL . 11 ,) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 21) . (#& . 20) . SEXP .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V3 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U2 .) (VARIABLE . GROUND . LISTP . LIL . NIL . (#& . 2) . U0 .) (5 . LISTP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 11) . (#& . 2) . LISTP .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . U3 .) (VARIABLE . GROUND , LISTP . NIL . NIL . (#& . 2) . V0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . V2 .) (VARIABLE & GROUND . LISTP . NIL . NIL . (#& . 2) . W .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 2) . W1 .) (VARIABLE & GROUND . LISTP . NIL . NIL . (#& . 2) . W3 .) (NIL . (DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) (OT& . GROUND) VARIABLE LISTP) . NIL . ((W3 #& . 3) (W1 #& . 4) (W #& . 5) (V2 #& . 6) (V0 #& . 7) (U3 #& . 8) (U1 #& . 9) (U #& . 1) (LISTP #& . 10) (U0 #& . 12) (U2 #& . 13) (V #& . 14) (V1 #& . 15) (V3 #& . 16) (W0 #& . 17) (W2 #& . 18)) . LIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 1 &) (VARIABLE . GROUND . LISTP . NIL . LIL . (#& . 2) . U .)  (((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((U #& . 1) (SEXP #& . 19)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 12 .))